Definitions | t T, {T}, P  Q, x:A. B(x), SQType(T), IdLnk, s = t, Prop, ||as||, s ~ t, False, A, A B, , {x:A| B(x) }, , x:A B(x), lnk(e), mlnk(m), <a,b>, es-M(es), f(a), Id, Type, x:A B(x), mtag(m), rcvtype(e), msgtype(m), b,  b, , isrcv(e), P & Q, P  Q, Unit, left+right, valtype(e), (Msg on l), ES, E, Msg, sends(l;e), a<b, #$n, Void, type List, S T, l[i], tag(e), haslink(l;m), Msg(M) |